<!DOCTYPE html>
<html lang="en-us">
  <head>
    <meta charset="utf-8">
    <meta http-equiv="X-UA-Compatible" content="IE=edge,chrome=1">
    
    <title>编程语言的形式语义 | Practice, Rethink, Improve</title>
    <meta name="viewport" content="width=device-width,minimum-scale=1">
    <meta name="description" content="计算机程序语义
你在编程序的时候，是否想过一个问题：计算机是怎么知道人们想要它做什么的呢？这个问题涉及到编程的本质，编程作为人类的一种活动，核心是编程语言，而对于一门语言，最重要的，必然是语义。">
    <meta name="generator" content="Hugo 0.89.4" />
    
    
      <META NAME="ROBOTS" CONTENT="NOINDEX, NOFOLLOW">
    

    
<link rel="stylesheet" href="/ananke/css/main.min.css" >




    
      

    

    
    
    <meta property="og:title" content="编程语言的形式语义" />
<meta property="og:description" content="计算机程序语义
你在编程序的时候，是否想过一个问题：计算机是怎么知道人们想要它做什么的呢？这个问题涉及到编程的本质，编程作为人类的一种活动，核心是编程语言，而对于一门语言，最重要的，必然是语义。" />
<meta property="og:type" content="article" />
<meta property="og:url" content="https://wanghuibin0.gitee.io/posts/2021-04-21-program-semantics/" /><meta property="article:section" content="posts" />
<meta property="article:published_time" content="2021-04-21T13:42:34+00:00" />
<meta property="article:modified_time" content="2021-04-21T13:42:34+00:00" />

<meta itemprop="name" content="编程语言的形式语义">
<meta itemprop="description" content="计算机程序语义
你在编程序的时候，是否想过一个问题：计算机是怎么知道人们想要它做什么的呢？这个问题涉及到编程的本质，编程作为人类的一种活动，核心是编程语言，而对于一门语言，最重要的，必然是语义。"><meta itemprop="datePublished" content="2021-04-21T13:42:34+00:00" />
<meta itemprop="dateModified" content="2021-04-21T13:42:34+00:00" />
<meta itemprop="wordCount" content="17">
<meta itemprop="keywords" content="编程语言,形式语义," /><meta name="twitter:card" content="summary"/>
<meta name="twitter:title" content="编程语言的形式语义"/>
<meta name="twitter:description" content="计算机程序语义
你在编程序的时候，是否想过一个问题：计算机是怎么知道人们想要它做什么的呢？这个问题涉及到编程的本质，编程作为人类的一种活动，核心是编程语言，而对于一门语言，最重要的，必然是语义。"/>

	
  </head>

  <body class="ma0 avenir bg-near-white">

    
   
  

  <header>
    <div class="bg-black">
      <nav class="pv3 ph3 ph4-ns" role="navigation">
  <div class="flex-l justify-between items-center center">
    <a href="/" class="f3 fw2 hover-white no-underline white-90 dib">
      
        Practice, Rethink, Improve
      
    </a>
    <div class="flex-l items-center">
      

      
      
















    </div>
  </div>
</nav>

    </div>
  </header>



    <main class="pb7" role="main">
      
  
  <article class="flex-l flex-wrap justify-between mw8 center ph3">
    <header class="mt4 w-100">
      <aside class="instapaper_ignoref b helvetica tracked">
          
        POSTS
      </aside>
      




  <div id="sharing" class="mt3">

    
    <a href="https://www.facebook.com/sharer.php?u=https://wanghuibin0.gitee.io/posts/2021-04-21-program-semantics/" class="facebook no-underline" aria-label="share on Facebook">
      <svg height="32px"  style="enable-background:new 0 0 67 67;" version="1.1" viewBox="0 0 67 67" width="32px" xml:space="preserve" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink"><path d="M28.765,50.32h6.744V33.998h4.499l0.596-5.624h-5.095  l0.007-2.816c0-1.466,0.14-2.253,2.244-2.253h2.812V17.68h-4.5c-5.405,0-7.307,2.729-7.307,7.317v3.377h-3.369v5.625h3.369V50.32z   M33,64C16.432,64,3,50.569,3,34S16.432,4,33,4s30,13.431,30,30S49.568,64,33,64z" style="fill-rule:evenodd;clip-rule:evenodd;"/></svg>

    </a>

    
    
    <a href="https://twitter.com/share?url=https://wanghuibin0.gitee.io/posts/2021-04-21-program-semantics/&amp;text=%e7%bc%96%e7%a8%8b%e8%af%ad%e8%a8%80%e7%9a%84%e5%bd%a2%e5%bc%8f%e8%af%ad%e4%b9%89" class="twitter no-underline" aria-label="share on Twitter">
      <svg height="32px"  style="enable-background:new 0 0 67 67;" version="1.1" viewBox="0 0 67 67" width="32px" xml:space="preserve" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink"><path d="M37.167,22.283c-2.619,0.953-4.274,3.411-4.086,6.101  l0.063,1.038l-1.048-0.127c-3.813-0.487-7.145-2.139-9.974-4.915l-1.383-1.377l-0.356,1.017c-0.754,2.267-0.272,4.661,1.299,6.271  c0.838,0.89,0.649,1.017-0.796,0.487c-0.503-0.169-0.943-0.296-0.985-0.233c-0.146,0.149,0.356,2.076,0.754,2.839  c0.545,1.06,1.655,2.097,2.871,2.712l1.027,0.487l-1.215,0.021c-1.173,0-1.215,0.021-1.089,0.467  c0.419,1.377,2.074,2.839,3.918,3.475l1.299,0.444l-1.131,0.678c-1.676,0.976-3.646,1.526-5.616,1.568  C19.775,43.256,19,43.341,19,43.405c0,0.211,2.557,1.397,4.044,1.864c4.463,1.377,9.765,0.783,13.746-1.568  c2.829-1.673,5.657-5,6.978-8.221c0.713-1.716,1.425-4.851,1.425-6.354c0-0.975,0.063-1.102,1.236-2.267  c0.692-0.678,1.341-1.419,1.467-1.631c0.21-0.403,0.188-0.403-0.88-0.043c-1.781,0.636-2.033,0.551-1.152-0.402  c0.649-0.678,1.425-1.907,1.425-2.267c0-0.063-0.314,0.042-0.671,0.233c-0.377,0.212-1.215,0.53-1.844,0.72l-1.131,0.361l-1.027-0.7  c-0.566-0.381-1.361-0.805-1.781-0.932C39.766,21.902,38.131,21.944,37.167,22.283z M33,64C16.432,64,3,50.569,3,34S16.432,4,33,4  s30,13.431,30,30S49.568,64,33,64z" style="fill-rule:evenodd;clip-rule:evenodd;fill:;"/></svg>

    </a>

    
    <a href="https://www.linkedin.com/shareArticle?mini=true&amp;url=https://wanghuibin0.gitee.io/posts/2021-04-21-program-semantics/&amp;title=%e7%bc%96%e7%a8%8b%e8%af%ad%e8%a8%80%e7%9a%84%e5%bd%a2%e5%bc%8f%e8%af%ad%e4%b9%89" class="linkedin no-underline" aria-label="share on LinkedIn">
      <svg  height="32px"  style="enable-background:new 0 0 65 65;" version="1.1" viewBox="0 0 65 65" width="32px" xml:space="preserve" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
  <path d="M50.837,48.137V36.425c0-6.275-3.35-9.195-7.816-9.195  c-3.604,0-5.219,1.983-6.119,3.374V27.71h-6.79c0.09,1.917,0,20.427,0,20.427h6.79V36.729c0-0.609,0.044-1.219,0.224-1.655  c0.49-1.22,1.607-2.483,3.482-2.483c2.458,0,3.44,1.873,3.44,4.618v10.929H50.837z M22.959,24.922c2.367,0,3.842-1.57,3.842-3.531  c-0.044-2.003-1.475-3.528-3.797-3.528s-3.841,1.524-3.841,3.528c0,1.961,1.474,3.531,3.753,3.531H22.959z M34,64  C17.432,64,4,50.568,4,34C4,17.431,17.432,4,34,4s30,13.431,30,30C64,50.568,50.568,64,34,64z M26.354,48.137V27.71h-6.789v20.427  H26.354z" style="fill-rule:evenodd;clip-rule:evenodd;fill:;"/>
</svg>

    </a>
  </div>


      <h1 class="f1 athelas mt3 mb1">编程语言的形式语义</h1>
      
      
      
      <time class="f6 mv4 dib tracked" datetime="2021-04-21T13:42:34Z">April 21, 2021</time>
      

      
      
    </header>
    <div class="nested-copy-line-height lh-copy serif f4 nested-links nested-img mid-gray pr4-l w-two-thirds-l"><h1 id="计算机程序语义">计算机程序语义</h1>
<p>你在编程序的时候，是否想过一个问题：计算机是怎么知道人们想要它做什么的呢？这个问题涉及到编程的本质，编程作为人类的一种活动，核心是编程语言，而对于一门语言，最重要的，必然是语义。</p>
<h2 id="编程语言">编程语言</h2>
<p>人与人之间的交流靠语言，人与计算机之间的交流也靠语言，只不过是更加严谨的计算机语言。语言有两大要素——语法和语义，语法是看得见的表面的形式，语义是真正想表达的背后的含义。各种五发八门的不同的编程语言，其表面形式可以天差地别，但其背后的语义却是相通的。只有使计算机「理解」了人类想表达的东西，才有可能准确给出人类想要的结果。当然也需要计算机拥有对应的计算能力，这正是计算理论所研究的内容，各种计算模型，如有限状态自动机，下推自动机，图灵机，确定性的，不确定性的等等，计算能力的确有差别。不过这一切的前提是你得想办法把自己的想法「告诉」计算机，这就绕不开计算机程序的语义。</p>
<h2 id="形式语义">形式语义</h2>
<p>形式语义试图精确地、无歧义地描述程序的含义，并利用这些含义研究程序的性质。现实中，程序的语义通常有两种方式描述：一种是靠实现规范，如Ruby解释器有一个参考实现；另一种是写一份平实的官方规范，如C++/Java/ECMAScript。</p>
<p>而从更加形式化也更加数学化的角度看，描述程序可以由三种语义：操作语义、指称语义和公理语义。</p>
<h3 id="操作语义">操作语义</h3>
<p>操作语义为程序在某种机器的执行定义一些规则，来捕捉编程语言的含义。这个机器通常是一种抽象的机器：为了解释这种语言所写的程序如何执行，而设计出来的一种想象的、理想化的计算机。操作语义又分为小步操作语义和大步操作语义。</p>
<h4 id="小步操作语义">小步操作语义</h4>
<p>假想一台机器，用这台机器直接按照这种语言的语法进行操作一小步ー小步地对其进行反复规约，从而对一个程序求值。这种语义相当于为程序实现了一种迭代式的解释器。</p>
<h4 id="大步操作语义">大步操作语义</h4>
<p>大步语义的思想是，定义如何从一个表达式或者语句直接得到它的结果。这必然需要把程序的执行当成一个递归的而不是迭代的过程。也就是说，为了对一个更大的表达式求值，我们要对所有比它小的子表达式求值，然后把结果结合起来得到最终答案。这种语义相当于为程序实现了一种递归式的解释器。</p>
<h3 id="指称语义">指称语义</h3>
<p>用一种更低级更形式化的语言，或者至少比被描述的语言更好理解的语言，来描述新的语言。它更抽象，与操作语义更像解释器相比，它更像编译器。</p>
<h3 id="公理语义">公理语义</h3>
<p>通过在语句执行前后，分别给出抽象机器状态的断言，来描述一个语句的含义：如果前置条件在语句执行前初始化为true，那么执行后的后置条件也保证为true。公理语义主要用于验证程序的正确性。</p><ul class="pa0">
  
   <li class="list">
     <a href="/tags/%E7%BC%96%E7%A8%8B%E8%AF%AD%E8%A8%80" class="link f5 grow no-underline br-pill ba ph3 pv2 mb2 dib black sans-serif">编程语言</a>
   </li>
  
   <li class="list">
     <a href="/tags/%E5%BD%A2%E5%BC%8F%E8%AF%AD%E4%B9%89" class="link f5 grow no-underline br-pill ba ph3 pv2 mb2 dib black sans-serif">形式语义</a>
   </li>
  
</ul>
<div class="mt6 instapaper_ignoref">
      
      
      </div>
    </div>

    <aside class="w-30-l mt6-l">




</aside>

  </article>

    </main>
    <footer class="bg-black bottom-0 w-100 pa3" role="contentinfo">
  <div class="flex justify-between">
  <a class="f4 fw4 hover-white no-underline white-70 dn dib-ns pv2 ph3" href="https://wanghuibin0.gitee.io/" >
    &copy;  Practice, Rethink, Improve 2021 
  </a>
    <div>















</div>
  </div>
</footer>

  </body>
</html>
